ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), a:ecl(ds; da), l:( List).
eclcatch(a; l)  ecl(ds; da) 

latex

Definitions	x. t(x), eclcatch(a; l), t  T, ecl(ds; da), x:A. B(x), x(s)
Lemmas	Id wf, fpf wf, Knd wf, bool wf, ma-valtype wf, decl-state wf, nat wf